data($T$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$x$:Id $\times$ ($T$($x$))